active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
F(mark(X)) → F(X)
ACTIVE(f(f(a))) → G(f(a))
C(active(X)) → C(X)
MARK(g(X)) → ACTIVE(g(mark(X)))
G(active(X)) → G(X)
MARK(c(X)) → ACTIVE(c(X))
G(mark(X)) → G(X)
ACTIVE(f(f(a))) → F(g(f(a)))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(g(X)) → G(mark(X))
MARK(g(X)) → MARK(X)
MARK(a) → ACTIVE(a)
ACTIVE(f(f(a))) → MARK(c(f(g(f(a)))))
MARK(f(X)) → F(mark(X))
C(mark(X)) → C(X)
ACTIVE(f(f(a))) → C(f(g(f(a))))
F(active(X)) → F(X)
MARK(f(X)) → MARK(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(mark(X)) → F(X)
ACTIVE(f(f(a))) → G(f(a))
C(active(X)) → C(X)
MARK(g(X)) → ACTIVE(g(mark(X)))
G(active(X)) → G(X)
MARK(c(X)) → ACTIVE(c(X))
G(mark(X)) → G(X)
ACTIVE(f(f(a))) → F(g(f(a)))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(g(X)) → G(mark(X))
MARK(g(X)) → MARK(X)
MARK(a) → ACTIVE(a)
ACTIVE(f(f(a))) → MARK(c(f(g(f(a)))))
MARK(f(X)) → F(mark(X))
C(mark(X)) → C(X)
ACTIVE(f(f(a))) → C(f(g(f(a))))
F(active(X)) → F(X)
MARK(f(X)) → MARK(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
G(active(X)) → G(X)
G(mark(X)) → G(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(mark(X)) → G(X)
Used ordering: Polynomial interpretation [25,35]:
G(active(X)) → G(X)
The value of delta used in the strict ordering is 8.
POL(active(x1)) = (2)x_1
POL(mark(x1)) = 4 + (2)x_1
POL(G(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
G(active(X)) → G(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(active(X)) → G(X)
The value of delta used in the strict ordering is 1/16.
POL(active(x1)) = 1/4 + (2)x_1
POL(G(x1)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
C(active(X)) → C(X)
C(mark(X)) → C(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
C(active(X)) → C(X)
Used ordering: Polynomial interpretation [25,35]:
C(mark(X)) → C(X)
The value of delta used in the strict ordering is 8.
POL(C(x1)) = (2)x_1
POL(active(x1)) = 4 + (2)x_1
POL(mark(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
C(mark(X)) → C(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
C(mark(X)) → C(X)
The value of delta used in the strict ordering is 1/16.
POL(C(x1)) = (1/4)x_1
POL(mark(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
F(mark(X)) → F(X)
F(active(X)) → F(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(mark(X)) → F(X)
Used ordering: Polynomial interpretation [25,35]:
F(active(X)) → F(X)
The value of delta used in the strict ordering is 8.
POL(active(x1)) = (2)x_1
POL(mark(x1)) = 4 + (2)x_1
POL(F(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
F(active(X)) → F(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(active(X)) → F(X)
The value of delta used in the strict ordering is 1/16.
POL(active(x1)) = 1/4 + (2)x_1
POL(F(x1)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ACTIVE(f(f(a))) → MARK(c(f(g(f(a)))))
MARK(c(X)) → ACTIVE(c(X))
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(f(f(a))) → MARK(c(f(g(f(a)))))
Used ordering: Polynomial interpretation [25,35]:
MARK(c(X)) → ACTIVE(c(X))
The value of delta used in the strict ordering is 1/8.
POL(active(x1)) = 0
POL(f(x1)) = 1/4
POL(a) = 0
POL(MARK(x1)) = 0
POL(c(x1)) = 0
POL(g(x1)) = 0
POL(mark(x1)) = 0
POL(ACTIVE(x1)) = (1/2)x_1
c(active(X)) → c(X)
c(mark(X)) → c(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
MARK(c(X)) → ACTIVE(c(X))
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MARK(f(X)) → MARK(X)
MARK(g(X)) → MARK(X)
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(f(X)) → MARK(X)
MARK(g(X)) → MARK(X)
The value of delta used in the strict ordering is 4.
POL(MARK(x1)) = (4)x_1
POL(f(x1)) = 1 + x_1
POL(g(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)